DROPS

Document

Invited Paper

DOI: 10.4230/LIPIcs.CONCUR.2018.2

Bisimulations for Probabilistic and Quantum Processes (Invited Paper)

Authors: Yuxin Deng

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract

Bisimulation is a fundamental concept in the classical concurrency theory for comparing the behaviour of nondeterministic processes. It admits elegant characterisations from various perspectives such as fixed point theory, modal logics, game theory, coalgebras etc. In this paper, we review some key ideas used in the formulations and characterisations of reasonable notions of bisimulations for both probabilistic and quantum processes. To some extent the transition from probabilistic to quantum concurrency theory is smooth and natural. However, new ideas need also to be introduced. We have not yet reached the stage of formally verifying quantum communication protocols and quantum algorithms using bisimulations implemented by automatic tools. We discuss some recent efforts in this direction.

Cite as

Yuxin Deng. Bisimulations for Probabilistic and Quantum Processes (Invited Paper). In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 2:1-2:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{deng:LIPIcs.CONCUR.2018.2,
  author =	{Deng, Yuxin},
  title =	{{Bisimulations for Probabilistic and Quantum Processes}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{2:1--2:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.2},
  URN =		{urn:nbn:de:0030-drops-95406},
  doi =		{10.4230/LIPIcs.CONCUR.2018.2},
  annote =	{Keywords: Bisimulations, probabilistic processes, quantum processes}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2015.427

On Coinduction and Quantum Lambda Calculi

Authors: Yuxin Deng, Yuan Feng, and Ugo Dal Lago

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract

In the ubiquitous presence of linear resources in quantum computation, program equivalence in linear contexts, where programs are used or executed once, is more important than in the classical setting. We introduce a linear contextual equivalence and two notions of bisimilarity, a state-based and a distribution-based, as proof techniques for reasoning about higher-order quantum programs. Both notions of bisimilarity are sound with respect to the linear contextual equivalence, but only the distribution-based one turns out to be complete. The completeness proof relies on a characterisation of the bisimilarity as a testing equivalence.

Cite as

Yuxin Deng, Yuan Feng, and Ugo Dal Lago. On Coinduction and Quantum Lambda Calculi. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 427-440, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{deng_et_al:LIPIcs.CONCUR.2015.427,
  author =	{Deng, Yuxin and Feng, Yuan and Dal Lago, Ugo},
  title =	{{On Coinduction and Quantum Lambda Calculi}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{427--440},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.427},
  URN =		{urn:nbn:de:0030-drops-53883},
  doi =		{10.4230/LIPIcs.CONCUR.2015.427},
  annote =	{Keywords: Quantum lambda calculi, contextual equivalence, bisimulation}
}

Search Results

Documents authored by Deng, Yuxin

Bisimulations for Probabilistic and Quantum Processes (Invited Paper)

Abstract

Cite as

On Coinduction and Quantum Lambda Calculi

Abstract

Cite as

Thanks for your feedback!

Could not send message